%----------------- TEXT -----------------
\subsection*{1.5. French}

\textbf{Lemme 1.5.}

Si $\mathcal{O}$ est complet, alors le triple $(\mathcal{O}, d, \Omega)$ est isomorphe au triple $$(k[[t]], \partial_t, k[[t]]\,dt).$$

Les homomorphismes induits par $d$
\[
\mathrm{Gr}(d) : \mathfrak{m}^i / \mathfrak{m}^{i+1} \longrightarrow \mathfrak{m}^{i-1} \Omega / \mathfrak{m}^i \Omega
\]
sont linéaires bijectifs (1.4.4). 

Puisque $\mathcal{O}$ est complet, $d : \mathfrak{m} \to \Omega$ est donc surjectif et $\ker(d) \xrightarrow{\sim} k$. 

Ceci nous fournit un corps de représentants annulé par $d$, et le choix d'une uniformisante $t$ fournit l'isomorphisme voulu $$k[[t]] \xrightarrow{\sim} \mathcal{O}.$$

%----------------- TRANSLATION -----------------
\newpage 

\subsection*{1.5. English}

\textbf{Lemma 1.5.}

If $\mathcal{O}$ is complete, then the triple $(\mathcal{O}, d, \Omega)$ is isomorphic to the triple $$(k[[t]], \partial_t, k[[t]]\,dt).$$

The maps induced by $d$
\[
\mathrm{Gr}(d) : \mathfrak{m}^i / \mathfrak{m}^{i+1} \longrightarrow \mathfrak{m}^{i-1} \Omega / \mathfrak{m}^i \Omega
\]
are linear isomorphisms (by (1.4.4)).

Since $\mathcal{O}$ is complete, the map $d : \mathfrak{m} \to \Omega$ is therefore surjective and $\ker(d) \xrightarrow{\sim} k$.

This provides a coefficient field annihilated by $d$, and the choice of a uniformizer $t$ yields the desired isomorphism $$k[[t]] \xrightarrow{\sim} \mathcal{O}.$$

